The major limitation of #1164 is that we can only use trivial functions as the second argument to animate, without the evaluator getting stuck. That is, functions where only a substitution is needed for the function body to reach a normal form.

Consider an expression animate 5 (λt. circle (t × 2)). Note that both arguments are normal forms. The problem is that evaluating this requires evaluating circle (0 × 2), circle (0.1 × 2), circle (0.2 × 2) etc. in order to generate the frames of the animation. Whereas for all of our other primitives, once the arguments are in normal form, computing the normal form of the applied function is trivial. This all happens in the function primFunDef, which establishes the semantics of our primitive functions, and is not set up to be able evaluate further. Even at a higher level, it's not clear how we should handle this, given that the new expressions requiring evaluation are not guaranteed to be normalizing.

This PR lifts the trivial-functions restriction in most circumstances, in a hacky unprincipled way. It breaks all sorts of abstractions, and doesn't guarantee that evaluation respects the configured termination bound. Of course, it should not be merged in anything resembling its current form, but it's useful for exploring more complex animations. A proper solution will require some sort of reworking of the evaluator, and I'm not yet sure what that should look like. Alternatively, and this is my personal preference, we could just embrace the projections-based approach discussed in #1173.